Termination Proof Script

• Consider the SCC {7}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 7 is strictly decreasing.


• Consider the SCC {6,8}. The usable rules are {3,4}. By taking the AF π with π(QUOT) = 1 together with the lexicographic path order with precedence plus ≻ s, rule 8 is weakly decreasing and the rules in {3,4,6} are strictly decreasing. There is one new SCC.
  • Consider the SCC {8}. By taking the AF π with π(QUOT) = 2, π(s) = [ ] and π(plus) = [2] together with the lexicographic path order with precedence 0 ≻ plus ≻ s, the rules in {3,4,8} are strictly decreasing.